In this paper, we study the composition of services so as to obtain runs satisfying a task specification in Linear Temporal Logic on finite traces (LTLf). We study the problem in the case services are nondeterministic and the LTLf specification can be exactly met, and in the case services are stochastic, where we are interested in maximizing the probability of satisfaction of the LTLf specification and, simultaneously, minimizing the utilization cost of the services. To do so, we combine techniques from LTLf synthesis, service composition \`a la Roman Model, reactive synthesis, and bi-objective lexicographic optimization on MDPs. This framework has several interesting applications, including Smart Manufacturing and Digital Twins.

A wide range of problems, from contingent and multiagent planning to process/service orchestration, can be viewed as games. In many of these, it is natural to spec- ify the possible behaviors procedurally. In this paper, we develop a logical framework for specifying these types of problems/games based on the situation calculus and ConGolog. The framework incorporates game-theoretic path quantifiers as in ATL. We show that the framework can be used to model such problems in a natural way. We also show how verification/synthesis techniques can be used to solve problems expressed in the framework. In particular, we develop a method for dealing with infinite state settings using fixpoint approximation and “characteristic graphs”.

In this paper we look at the problem of composing services that export their behavior in terms of a transition system, characterizing the choices of actions given to a client at each point in time. The composition consists of synthesizing an orchestrator that coordinates the available services so as to mimic the desired target service asked by the client. Specifically, in this paper we study the "conformant form" of the problem, where available services are partially controllable and partially observable, and hence, the orchestrator has to make its decisions exploiting the observations made so far only. We give a sound and complete procedure to synthesize the orchestrator in such case, and characterize the computational complexity of the problem. The procedure is based on working with belief (or knowledge) states, a standard technique to tackle conformant planning. Moreover we show that, although in general unavoidable, the powerset construction at the base of the belief state approach can be delegated to the symbolic manipulations of the game-structure model checking tool (TLV), which can be used to efficiently implement the orchestrator synthesis procedure.